1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. $\forall$$x$:$T$. ($x$ $\in$ $v$) $\Rightarrow$ ($\neg$($x$ = last($v$))) $\Rightarrow$ $x$ before last($v$) $\in$ $v$
\\[0ex]6. $x$ : $T$
\\[0ex]7. $x$ = $u$
\\[0ex]8. $v$ = []
\\[0ex]9. $z$ : $T$ List
\\[0ex]$\vdash$  $\neg$($\uparrow$null([$u$ / $z$]))